| 1: | a__eq(0,0) | → true | |
| 2: | a__eq(s(X),s(Y)) | → a__eq(X,Y) | |
| 3: | a__eq(X,Y) | → false | |
| 4: | a__inf(X) | → cons(X,inf(s(X))) | |
| 5: | a__take(0,X) | → nil | |
| 6: | a__take(s(X),cons(Y,L)) | → cons(Y,take(X,L)) | |
| 7: | a__length(nil) | → 0 | |
| 8: | a__length(cons(X,L)) | → s(length(L)) | |
| 9: | mark(eq(X1,X2)) | → a__eq(X1,X2) | |
| 10: | mark(inf(X)) | → a__inf(mark(X)) | |
| 11: | mark(take(X1,X2)) | → a__take(mark(X1),mark(X2)) | |
| 12: | mark(length(X)) | → a__length(mark(X)) | |
| 13: | mark(0) | → 0 | |
| 14: | mark(true) | → true | |
| 15: | mark(s(X)) | → s(X) | |
| 16: | mark(false) | → false | |
| 17: | mark(cons(X1,X2)) | → cons(X1,X2) | |
| 18: | mark(nil) | → nil | |
| 19: | a__eq(X1,X2) | → eq(X1,X2) | |
| 20: | a__inf(X) | → inf(X) | |
| 21: | a__take(X1,X2) | → take(X1,X2) | |
| 22: | a__length(X) | → length(X) | |
| 23: | A__EQ(s(X),s(Y)) | → A__EQ(X,Y) | |
| 24: | MARK(eq(X1,X2)) | → A__EQ(X1,X2) | |
| 25: | MARK(inf(X)) | → A__INF(mark(X)) | |
| 26: | MARK(inf(X)) | → MARK(X) | |
| 27: | MARK(take(X1,X2)) | → A__TAKE(mark(X1),mark(X2)) | |
| 28: | MARK(take(X1,X2)) | → MARK(X1) | |
| 29: | MARK(take(X1,X2)) | → MARK(X2) | |
| 30: | MARK(length(X)) | → A__LENGTH(mark(X)) | |
| 31: | MARK(length(X)) | → MARK(X) | |